# Definitional laws for Color layer 1.
#
# Honest scope: Base F32 primitives (add/mul/div/show/cmp/clamp/...) are opaque
# to definitional equality. Therefore rgb_to_hsl / hsl_to_rgb roundtrips,
# F32.clamp-based field updates, and Color.range_valid (which uses F32.is_le on
# alpha) are NOT stated as {==} laws. Runtime smoke for converts lives in
# main.bend. Laws below are only claims that normalize under Bend 2.0.2.
import Base
import ./lib.bend as C

# Constructors equal their data literals.
law rgb_ctor:
  { C.Color.rgb(10, 20, 30, 1.0) == C.Rgb{10, 20, 30, 1.0} : C.Rgb }

law hsl_ctor:
  { C.Color.hsl(120.0, 1.0, 0.5, 1.0) == C.Hsl{120.0, 1.0, 0.5, 1.0} : C.Hsl }

law range_ctor:
  {
    C.Color.range(C.Color.rgb(0, 0, 0, 0.0), C.Color.rgb(1, 2, 3, 1.0))
      == C.ColorRange{C.Rgb{0, 0, 0, 0.0}, C.Rgb{1, 2, 3, 1.0}}
    : C.ColorRange
  }

# Constructor projections.
law rgb_r_proj:
  { C.Color.rgb_r(C.Color.rgb(10, 20, 30, 1.0)) == 10 : U32 }

law rgb_g_proj:
  { C.Color.rgb_g(C.Color.rgb(10, 20, 30, 1.0)) == 20 : U32 }

law rgb_b_proj:
  { C.Color.rgb_b(C.Color.rgb(10, 20, 30, 1.0)) == 30 : U32 }

law rgb_a_proj:
  { C.Color.rgb_a(C.Color.rgb(10, 20, 30, 0.5)) == 0.5 : F32 }

law hsl_h_proj:
  { C.Color.hsl_h(C.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 240.0 : F32 }

law hsl_s_proj:
  { C.Color.hsl_s(C.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 0.25 : F32 }

law hsl_l_proj:
  { C.Color.hsl_l(C.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 0.75 : F32 }

law hsl_a_proj:
  { C.Color.hsl_a(C.Color.hsl(240.0, 0.25, 0.75, 0.25)) == 0.25 : F32 }

# U32 clamp helpers.
law clamp_u8_low:
  { C.Color.clamp_u8(0) == 0 : U32 }

law clamp_u8_mid:
  { C.Color.clamp_u8(128) == 128 : U32 }

law clamp_u8_high:
  { C.Color.clamp_u8(255) == 255 : U32 }

law clamp_u8_overflow:
  { C.Color.clamp_u8(300) == 255 : U32 }

law clamp_u8_way_over:
  { C.Color.clamp_u8(1000) == 255 : U32 }

# clamp_rgb: only octet projections are definitional (alpha uses F32.clamp).
law clamp_rgb_r_overflow:
  { C.Color.rgb_r(C.Color.clamp_rgb(C.Color.rgb(300, 10, 400, 1.0))) == 255 : U32 }

law clamp_rgb_g_ok:
  { C.Color.rgb_g(C.Color.clamp_rgb(C.Color.rgb(300, 10, 400, 1.0))) == 10 : U32 }

law clamp_rgb_b_overflow:
  { C.Color.rgb_b(C.Color.clamp_rgb(C.Color.rgb(300, 10, 400, 1.0))) == 255 : U32 }

# Stable rgba/hsla string shape. U32.show reduces; F32.show stays symbolic,
# so both sides keep matching F32.show calls.
law rgba_string_red:
  {
    C.Color.to_rgba_string(C.Color.rgb(255, 0, 0, 1.0))
      == ("rgba(255,0,0," ++ F32.show(1.0) ++ ")")
    : String
  }

law rgba_string_black:
  {
    C.Color.to_rgba_string(C.Color.rgb(0, 0, 0, 0.0))
      == ("rgba(0,0,0," ++ F32.show(0.0) ++ ")")
    : String
  }

law rgba_string_custom:
  {
    C.Color.to_rgba_string(C.Color.rgb(12, 34, 56, 0.5))
      == ("rgba(12,34,56," ++ F32.show(0.5) ++ ")")
    : String
  }

law rgba_starts_with_prefix:
  {
    String.starts_with(
      C.Color.to_rgba_string(C.Color.rgb(255, 128, 64, 1.0)),
      "rgba(")
      == True{}
    : Bool
  }

law hsla_string_green:
  {
    C.Color.to_hsla_string(C.Color.hsl(120.0, 1.0, 0.5, 1.0))
      == ("hsla(" ++ F32.show(120.0) ++ "," ++ F32.show(1.0) ++ ","
          ++ F32.show(0.5) ++ "," ++ F32.show(1.0) ++ ")")
    : String
  }

law hsla_string_zero:
  {
    C.Color.to_hsla_string(C.Color.hsl(0.0, 0.0, 0.0, 0.0))
      == ("hsla(" ++ F32.show(0.0) ++ "," ++ F32.show(0.0) ++ ","
          ++ F32.show(0.0) ++ "," ++ F32.show(0.0) ++ ")")
    : String
  }