use crate::generate::archetypes::TestInput;
use crate::spec::types::OpSpec;
use crate::spec::AlgebraicLaw;
use crate::spec::Property;
use super::values::{
byte_expr, bytes_literal, input_words, value_inputs_expr, value_inputs_from_words,
};
use crate::generate::emit::cross_product::Route;
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub(super) enum LawShape {
RunEqRun,
RunEqLiteral,
Associative,
Involution,
Bounded,
}
pub(super) fn law_shape(route: &Route) -> LawShape {
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Associative => LawShape::Associative,
AlgebraicLaw::Identity { .. }
| AlgebraicLaw::SelfInverse { .. }
| AlgebraicLaw::Idempotent
| AlgebraicLaw::Absorbing { .. } => LawShape::RunEqLiteral,
AlgebraicLaw::Involution => LawShape::Involution,
AlgebraicLaw::Bounded { .. } => LawShape::Bounded,
_ => LawShape::RunEqRun,
}
}
_ => LawShape::RunEqRun,
}
}
pub(super) fn law_label(property: &Property) -> String {
match property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Commutative => "commutativity".to_string(),
AlgebraicLaw::Associative => "associativity".to_string(),
AlgebraicLaw::Identity { .. } => "right identity".to_string(),
AlgebraicLaw::SelfInverse { .. } => "self-inverse".to_string(),
AlgebraicLaw::Idempotent => "idempotence".to_string(),
AlgebraicLaw::Absorbing { .. } => "right absorbing".to_string(),
AlgebraicLaw::Involution => "involution".to_string(),
AlgebraicLaw::Bounded { .. } => "bounded".to_string(),
other => other.name().to_string(),
}
}
_ => "point parity".to_string(),
}
}
pub(super) fn law_lhs_inputs(op: &OpSpec, input: &TestInput, route: &Route) -> String {
let words = input_words(op, input);
let a = words.first().copied().unwrap_or(0);
let b = words.get(1).copied().unwrap_or(a);
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Commutative => value_inputs_from_words(&[a, b]),
_ => value_inputs_from_words(&[a, b]),
}
}
_ => value_inputs_from_words(&[a, b]),
}
}
pub(super) fn law_rhs_inputs(op: &OpSpec, input: &TestInput, route: &Route) -> String {
let words = input_words(op, input);
let a = words.first().copied().unwrap_or(0);
let b = words.get(1).copied().unwrap_or(a);
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Commutative => value_inputs_from_words(&[b, a]),
_ => value_inputs_from_words(&[a, b]),
}
}
_ => value_inputs_from_words(&[a, b]),
}
}
pub(super) fn law_input_values(op: &OpSpec, input: &TestInput, route: &Route) -> String {
let words = input_words(op, input);
let a = words.first().copied().unwrap_or(0);
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Identity { element } => value_inputs_from_words(&[a, *element]),
AlgebraicLaw::SelfInverse { .. } | AlgebraicLaw::Idempotent => {
value_inputs_from_words(&[a, a])
}
AlgebraicLaw::Absorbing { element } => value_inputs_from_words(&[a, *element]),
_ => value_inputs_expr(op, input),
}
}
_ => value_inputs_expr(op, input),
}
}
pub(super) fn law_output_values(input: &TestInput, route: &Route) -> String {
let a = input.values.first().copied().unwrap_or(0);
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match &law.law {
AlgebraicLaw::Identity { element }
| AlgebraicLaw::SelfInverse { result: element }
| AlgebraicLaw::Absorbing { element } => bytes_literal(&element.to_le_bytes()),
AlgebraicLaw::Idempotent => bytes_literal(&a.to_le_bytes()),
_ => "Vec::<u8>::new()".to_string(),
}
}
_ => "Vec::<u8>::new()".to_string(),
}
}
pub(super) fn associative_ab_inputs(op: &OpSpec, input: &TestInput) -> String {
let words = input_words(op, input);
value_inputs_from_words(&[
words.first().copied().unwrap_or(0),
words.get(1).copied().unwrap_or(0),
])
}
pub(super) fn associative_bc_inputs(op: &OpSpec, input: &TestInput) -> String {
let words = input_words(op, input);
value_inputs_from_words(&[
words.get(1).copied().unwrap_or(0),
words.get(2).copied().unwrap_or(1),
])
}
pub(super) fn associative_lhs_inputs(input: &TestInput, expected_bytes: usize) -> String {
let c = input.values.get(2).copied().unwrap_or(1);
let lhs_bytes = (0..expected_bytes)
.map(|i| format!("ab.to_le_bytes()[{}], {}", i, byte_expr(c, i)))
.collect::<Vec<_>>()
.join(", ");
let zero_pad = (0..expected_bytes)
.map(|_| "0x00u8".to_string())
.collect::<Vec<_>>()
.join(", ");
format!(
"vec![vyre_conform::spec::value::Value::Bytes(vec![{lhs_bytes}]), vyre_conform::spec::value::Value::Bytes(vec![{zero_pad}])]"
)
}
pub(super) fn associative_rhs_inputs(input: &TestInput, expected_bytes: usize) -> String {
let a = input.values.first().copied().unwrap_or(0);
let rhs_bytes = (0..expected_bytes)
.map(|i| format!("{}, bc.to_le_bytes()[{}]", byte_expr(a, i), i))
.collect::<Vec<_>>()
.join(", ");
let zero_pad = (0..expected_bytes)
.map(|_| "0x00u8".to_string())
.collect::<Vec<_>>()
.join(", ");
format!(
"vec![vyre_conform::spec::value::Value::Bytes(vec![{rhs_bytes}]), vyre_conform::spec::value::Value::Bytes(vec![{zero_pad}])]"
)
}
pub(super) fn involution_first_inputs(input: &TestInput) -> String {
value_inputs_from_words(&[input.values.first().copied().unwrap_or(0)])
}
pub(super) fn involution_expected(input: &TestInput) -> String {
bytes_literal(&input.values.first().copied().unwrap_or(0).to_le_bytes())
}
pub(super) fn bounded_lo(route: &Route) -> u32 {
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match law.algebraic_law() {
AlgebraicLaw::Bounded { lo, .. } => *lo,
_ => 0,
}
}
_ => 0,
}
}
pub(super) fn bounded_hi(route: &Route) -> u32 {
match &route.property {
Property::DeclaredLawHolds { law } | Property::CompositionPreservesLaw { law } => {
match law.algebraic_law() {
AlgebraicLaw::Bounded { hi, .. } => *hi,
_ => u32::MAX,
}
}
_ => u32::MAX,
}
}