module EnigmaBroke where

type Rotor       = [26](Char, Bit)

mkRotor : {a} (fin a) => ([26]Char,[a]) -> Rotor
mkRotor (_,_) = zero

scramble : (Bit, Char, Rotor) -> (Bit, Char, Rotor)
scramble (_,_,_) = zero

joinRotors : {n} (fin n) => ([n]Rotor, Char) -> ([n]Rotor, Char)
joinRotors (rotors, inputChar) = (rotors', outputChar)
  where
    initRotor = mkRotor (['A' .. 'Z'], [])
    // ncrs : [n+1](Bit, [8], Rotor)
    ncrs = [(True, inputChar, initRotor)]
               # [ scramble (notch, char, r)
                 | r <- rotors
                 | (notch, char, rotor') <- ncrs
                 ]
    rotors' = tail [ r | (_, _, r) <- ncrs ]
    (_, outputChar, _) = ncrs ! 0