shipping_cost.iml

(*
   --------------------------------------------------------------------------
   title: Shipping Cost Calculator
   name: shipping-cost
   description: Calculate shipping cost with weight, distance, and tier
   --------------------------------------------------------------------------
 
   Real-world example: E-commerce Shipping Cost Calculator
 
   Use case: Calculate shipping cost based on weight, distance, and customer tier.
 
   Practical implications:
   - Ensures correct pricing for all shipping scenarios
   - Identifies edge cases in promotion logic
   - Provides test cases for order processing
   - Helps verify business rules are implemented correctly
   - Critical for revenue management
*)
 
type customer_tier = Premium | Standard | Basic
 
(* Base shipping rate per kg based on distance *)
let base_rate_per_kg distance_km =
  if distance_km <= 50 then
    2
  else if distance_km <= 200 then
    3
  else
    5
 
(* Rewrite rule: distance-based optimization *)
let distance_rule x =
  x * 2 = x + x
[@@rw] [@@imandra_rule_spec]
 
(* Calculate shipping cost *)
let calculate_shipping weight_kg distance_km tier =
  if weight_kg <= 0 || distance_km <= 0 then
    (* Invalid input *)
    0
  else
    let rate = base_rate_per_kg distance_km in
    let base_cost = weight_kg * rate in
    (* Apply customer tier discount *)
    if tier = Premium then
      (* Premium: free shipping over $50, else 50% off *)
      if base_cost > 50 then
        0
      else
        base_cost / 2
    else if tier = Standard then
      (* Standard: 20% off *)
      (base_cost * 4) / 5
    else
      (* Basic: full price, but min $5 *)
      if base_cost < 5 then
        5
      else
        base_cost
[@@decomp top ~basis:[[%id base_rate_per_kg]] ~rule_specs:[[%id distance_rule]] ()]
 
(* Variation: With pruning *)
let calculate_shipping_valid weight_kg distance_km tier =
  let rate = base_rate_per_kg distance_km in
  let base_cost = weight_kg * rate in
  if tier = Premium then
    if base_cost > 50 then 0
    else base_cost / 2
  else if tier = Standard then
    (base_cost * 4) / 5
  else
    if base_cost < 5 then 5
    else base_cost
[@@decomp top ~prune:true ~basis:[[%id base_rate_per_kg]] ()]
 
(* Variation: Context simplification to see tier-specific logic more clearly *)
let calculate_shipping_simp weight_kg distance_km tier =
  let rate = base_rate_per_kg distance_km in
  let base_cost = weight_kg * rate in
  if tier = Premium then
    if base_cost > 50 then 0
    else base_cost / 2
  else if tier = Standard then
    (base_cost * 4) / 5
  else
    if base_cost < 5 then 5
    else base_cost
[@@decomp top ~ctx_simp:true ~basis:[[%id base_rate_per_kg]] ()]