# [Year 2015 Day 11](https://adventofcode.com/2015/day/11)

This day provides a gentle introduction to refinement types, types which augment
other types with a predicate that must hold for all the values of the refined
type, which allow easily defining types as subsets of other types based on some
property of the acceptable elements.

While refinement types are quite easy to implement in Idris, and we easily could
implement the one we need for today's task as a throw away data structure just
for this module, we will be using the `refined`[^1] library's implementation for
the sake of getting on with it.

<!-- idris 
module Years.Y2015.Day11

import Control.Eff

import Runner
-->

```idris
import Data.Vect
import Data.String
import Data.Refined.Char

import Util
```

## Data Structures and Parsing

Provide a predicate which establishes that a char is a lowercase alphabetic
character, the only type of character that passwords are allowed to contain. We
use the `FromTo` predicate from the `refined`[^1] library to restrict chars to
within the range from `a` to `z`.

This predicate has multiplicity 0, a full discussion of multiplicites and linear
types is out of scope for today, but put simply this enforces that a value of
this predicate type can be "used" at most 0 times, having the effect of erasing
the value at runtime, making this more or less a zero-cost abstraction.

```idris
0 IsPasswordChar : Char -> Type
IsPasswordChar = FromTo 'a' 'z'
```

Combine a `Char` with its corresponding `IsPasswordChar` predicate into a
combined "refined" type, whose elements are the subset of `Char`s that are
lowercase alphabetic characters.

```idris
record PasswordChar where
  constructor MkPC
  char : Char
  {auto 0 prf : IsPasswordChar char}
%name PasswordChar pc
```

<!-- idris
Show PasswordChar where
  show (MkPC char) = singleton char

Eq PasswordChar where
  x == y = x.char == y.char
-->

A function to fallible convert `Char`s into refined `PasswordChar`s, this will
return `Just` if the `Char` satisfies the predicate, and `Nothing` otherwise,
aligning with the type-level guarantees of the `PasswordChar` type.

```idris
refineChar : Char -> Maybe PasswordChar
refineChar c = map fromSubset $ refine0 c
  where
    fromSubset : Subset Char IsPasswordChar -> PasswordChar
    fromSubset (Element char prf) = MkPC char
```

Convenience function returning `a` as a `PasswordChar`

```idris
lowest : PasswordChar
lowest = MkPC 'a'
```

"Increment" a `PasswordChar`, changing it to the next letter (`a` becomes `b`,
`b` becomes `c`, so on), returning nothing if we go past `z`, corresponding to a
carry.

We do this by converting the internal `Char` to an integer, adding one to it,
then converting back to a `Char`. This low-level conversion loses the refinement
context, forcing us to call `refineChar` on the new value to bring it back into
the refined type, providing us type-level assurance that this function will
return `Nothing` if an overflow occurs.

```idris
incriment : PasswordChar -> Maybe PasswordChar
incriment (MkPC char) = 
  let next = chr $ ord char + 1
  in refineChar next
```

A `Password` is a `Vect` of 8 `PasswordChar`s. This `Vect` is sorted in reverse
order compared to the `String` it corresponds to, with the right-most letter
first, to make implementing the `incrimentPassword` function a little easier and
cleaner.

We also provide conversion to/from a `String`

```idris
Password : Type
Password = Vect 8 PasswordChar
  
parsePassword : Has (Except String) fs => String -> Eff fs Password
parsePassword str = do
  cs <- note "Password has incorrect number of characters: \{str}" 
        . toVect 8 . reverse . unpack $ str
  cs <- note "Password contained invalid characters: \{str}" 
        $ traverse refineChar cs
  pure cs

passwordToString : Password -> String
passwordToString = pack . toList . reverse . map char
```

Define a function to increment a `Password`, this function will "roll over",
producing `aaaaaaaa` if provided `zzzzzzzz`.

```idris
incrimentPassword : Vect n PasswordChar -> Vect n PasswordChar
incrimentPassword [] = []
incrimentPassword (x :: xs) = 
  case incriment x of
    Nothing => lowest :: incrimentPassword xs
    Just x => x :: xs
```

### Password validity

A password must contain a run of at least 3 incrementing characters, check this
by converting the `PasswordChar`s to their integer representations. Remember
that our `Password` `Vect` is backwards compared to the string representation.

```idris
incrimentingChars : Vect n PasswordChar -> Bool
incrimentingChars (z :: next@(y :: (x :: xs))) = 
  let [x, y, z] : Vect _ Int = map (ord . char) [x, y, z]
  in if y == x + 1 && z == y + 1
    then True
    else incrimentingChars next
incrimentingChars _ = False
```

A password may not contain `i`, `o`, or `l`

```idris
noInvalidChars : Vect n PasswordChar -> Bool
noInvalidChars = not . (any (flip contains $ ['i', 'o', 'l'])) . map char
```

A password contains at least two different non-overlapping pairs.

We check this by pattern matching our password two characters at a time,
consuming both characters if a matched pair is found, and tacking on the `Char`
the list is composed of to an accumulator list as we go. This list is then
reduced to only its unique elements (it's `nub`), and checking to see if it's
length is at least 2.

```idris
containsPairs : Vect n PasswordChar -> Bool
containsPairs xs = length (nub $ pairs (reverse xs) []) >= 2
  where
    pairs : Vect m PasswordChar -> (acc : List Char) -> List Char
    pairs [] acc = acc
    pairs (x :: []) acc = acc
    pairs (x :: (y :: xs)) acc = 
      if x == y 
        -- If there is a pair, consume it to prevent detecting overlapping pairs
        then pairs xs (x.char :: acc)
        -- If there isn't a pair, only consume one character
        else pairs (y :: xs) acc
```

Combine our password criteria into one function

```idris
passwordCriteria : Vect n PasswordChar -> Bool
passwordCriteria xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
```

### Find the next password

Find the next password based on a criteria function

```idris
findNextPassword : 
  (f : Vect n PasswordChar -> Bool) -> (password : Vect n PasswordChar)
  -> Vect n PasswordChar
findNextPassword f password = 
  let next = incrimentPassword password
  in if f next
    then next
    else findNextPassword f next
```

## Part Functions

### Part 1

```idris
part1 : Eff (PartEff String) (String, Password)
part1 = do
  input <- map trim $ askAt "input"
  password <- parsePassword input
  info "Starting password: \{show password} -> \{passwordToString password}"
  let next_password = findNextPassword passwordCriteria password
  pure (passwordToString next_password, next_password)
```

### Part 2

```idris
part2 : Password -> Eff (PartEff String) String
part2 password = do
  info 
    "Second starting password: \{show password} -> \{passwordToString password}"
  let next_password = findNextPassword passwordCriteria password
  pure $ passwordToString next_password
```

<!-- idris
public export
day11 : Day
day11 = Both 11 part1 part2
-->

## References

[^1]: https://github.com/stefan-hoeck/idris2-refined/