inductive Color where
  | R | G | B | E
  deriving Repr, DecidableEq

structure Counts where
  r : Nat
  g : Nat
  b : Nat
  e : Nat
  deriving Repr

def countsZero (c : Counts) : Bool :=
  c.r == 0 && c.g == 0 && c.b == 0 && c.e == 0

def decCount (c : Counts) (col : Color) : Counts :=
  match col with
  | Color.R => { c with r := c.r - 1 }
  | Color.G => { c with g := c.g - 1 }
  | Color.B => { c with b := c.b - 1 }
  | Color.E => { c with e := c.e - 1 }

-- allowed choices given remaining counts and previous placed color
def allowed (counts : Counts) (prev : Option Color) : List Color :=
  let ok (col : Color) (avail : Nat) : Bool :=
    avail > 0 &&
    match prev with
    | none => true
    | some p => (p != col) || (col == Color.E) -- empties may repeat; colored must differ
  ([Color.R, Color.G, Color.B, Color.E]).filter fun col =>
    match col with
    | Color.R => ok Color.R counts.r
    | Color.G => ok Color.G counts.g
    | Color.B => ok Color.B counts.b
    | Color.E => ok Color.E counts.e

partial def build (rem : Nat) (prev : Option Color) (counts : Counts) : List (List Color) :=
  if rem == 0 then
    if countsZero counts then [ [] ] else []
  else
    let choices := allowed counts prev
    -- avoid using `List.bind` in case of name-resolution differences;
    -- build result by folding over choices and appending mapped tails
    choices.foldl (fun acc c =>
      let counts' := decCount counts c
      let tails := build (rem - 1) (some c) counts'
      acc ++ (tails.map fun t => c :: t)
    ) []

def showColor : Color -> String
  | Color.R => "R"
  | Color.G => "G"
  | Color.B => "B"
  | Color.E => "."

def main : IO Unit := do
  let initial : Counts := { r := 2, g := 2, b := 2, e := 3 }
  let solutions := build 9 none initial
  IO.println s!"Found {solutions.length} solutions (each printed as a 9-length sequence; '.' = empty)"
  for s in solutions do
    IO.println (String.intercalate " " (s.map showColor))

module Main where

data Color = R | G | B | E
  deriving (Eq, Show)

data Counts = Counts
  { cr :: Int
  , cg :: Int
  , cb :: Int
  , ce :: Int
  } deriving (Show)

countsZero :: Counts -> Bool
countsZero (Counts r g b e) = r == 0 && g == 0 && b == 0 && e == 0

decCount :: Counts -> Color -> Counts
decCount c col = case col of
  R -> c { cr = cr c - 1 }
  G -> c { cg = cg c - 1 }
  B -> c { cb = cb c - 1 }
  E -> c { ce = ce c - 1 }

allowed :: Counts -> Maybe Color -> [Color]
allowed counts prev = filter ok [R, G, B, E]
  where
    avail c = case c of
      R -> cr counts
      G -> cg counts
      B -> cb counts
      E -> ce counts
    ok c =
      avail c > 0 &&
      case prev of
        Nothing -> True
        Just p  -> (p /= c) || (c == E)  -- empties may repeat; colored must differ

-- build positions: rem = remaining slots to fill
build :: Int -> Maybe Color -> Counts -> [[Color]]
build 0 _ counts = if countsZero counts then [[]] else []
build rem prev counts =
  concatMap extend (allowed counts prev)
  where
    extend c = map (c :) (build (rem - 1) (Just c) (decCount counts c))

showColor :: Color -> String
showColor R = "R"
showColor G = "G"
showColor B = "B"
showColor E = "."

main :: IO ()
main = do
  let initial = Counts { cr = 2, cg = 2, cb = 2, ce = 3 }
      solutions = build 9 Nothing initial
  putStrLn $ "Found " ++ show (length solutions) ++ " solutions ('.' = empty)"
  mapM_ (putStrLn . unwords . map showColor) solutions

use std::fmt;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum Color {
    R,
    G,
    B,
    E,
}

impl fmt::Display for Color {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let s = match self {
            Color::R => "R",
            Color::G => "G",
            Color::B => "B",
            Color::E => ".",
        };
        write!(f, "{}", s)
    }
}

#[derive(Clone, Copy, Debug)]
struct Counts {
    r: u32,
    g: u32,
    b: u32,
    e: u32,
}

impl Counts {
    fn zero(&self) -> bool {
        self.r == 0 && self.g == 0 && self.b == 0 && self.e == 0
    }
}

/// decrement one count of `col` (caller must ensure availability > 0)
fn dec_count(mut c: Counts, col: Color) -> Counts {
    match col {
        Color::R => c.r -= 1,
        Color::G => c.g -= 1,
        Color::B => c.b -= 1,
        Color::E => c.e -= 1,
    }
    c
}

/// allowed choices given remaining counts and previous placed color
fn allowed(counts: Counts, prev: Option<Color>) -> Vec<Color> {
    let mut v = Vec::new();
    let ok = |col: Color, avail: u32| -> bool {
        if avail == 0 {
            return false;
        }
        match prev {
            None => true,
            Some(p) => p != col || col == Color::E, // empties may repeat; colored must differ
        }
    };
    if ok(Color::R, counts.r) {
        v.push(Color::R);
    }
    if ok(Color::G, counts.g) {
        v.push(Color::G);
    }
    if ok(Color::B, counts.b) {
        v.push(Color::B);
    }
    if ok(Color::E, counts.e) {
        v.push(Color::E);
    }
    v
}

/// backtracking builder
fn backtrack(
    rem: usize,
    prev: Option<Color>,
    counts: Counts,
    current: &mut Vec<Color>,
    solutions: &mut Vec<Vec<Color>>,
) {
    if rem == 0 {
        if counts.zero() {
            solutions.push(current.clone());
        }
        return;
    }

    for col in allowed(counts, prev) {
        let counts_next = dec_count(counts, col);
        current.push(col);
        backtrack(rem - 1, Some(col), counts_next, current, solutions);
        current.pop();
    }
}

fn main() {
    let initial = Counts {
        r: 2,
        g: 2,
        b: 2,
        e: 3,
    };
    let mut solutions: Vec<Vec<Color>> = Vec::new();
    let mut current: Vec<Color> = Vec::with_capacity(9);
    backtrack(9, None, initial, &mut current, &mut solutions);

    println!(
        "Found {} solutions (each printed as a 9-length sequence; '.' = empty)",
        solutions.len()
    );
    solutions.iter().for_each(|s| {
        let line = s.iter()
                .map(|c| c.to_string())
                .collect::<Vec<_>>()
                .join(" ");
        println!("{}", line);
    });

}