advent/src/Years/Y2015/Day5.md

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

This day provides a nice chance to introduce
[views](https://idris2.readthedocs.io/en/latest/tutorial/views.html),
specifically `String`'s
[`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList)
view, which lets us treat `String`s as if they were lazy lists or iterators.

```idris hide
module Years.Y2015.Day5

import Control.Eff

import Runner
```

```idris
import Data.String

import Util
```

```idris hide
%default total
```

## Nice Strings

### Contains at least 3 vowels

First we must define what a vowel is

```idris
vowels : List Char
vowels = ['a', 'e', 'i', 'o', 'u']
```

Now define a function to check if a string contains a minimum number of vowels.
Here we make use of the `with` rule and the `AsList` view over strings.

The `with` rule provides dependently typed pattern matching, allowing us to make
use of the fact that the form of some of the arguments can be determined by the
values of the others.

The `AsList` view associates a `String` with a lazy list of the characters in
the string by providing incremental proofs that the `String` decomposes into the
lazy list. An `AsList` of value `Nil`/`[]` proves that the associated string is
empty, and an `AsList` of value `c :: xs` proves that the associated string can
be generated by `strCons`ing the character `c` onto the rest of the string as
captured by the `AsList` in `xs`.

We use the `asList` function, which generates the `AsList` view for the provided
string, as the argument to the `with` block. Functions like this that produce
views for a value are refereed to as "covering functions". In general, views are
dependently typed constructs whose value provides insight into the structure of
another value.

We implement this function by keeping a counter of the number of vowels we still
need to see to accept the string, returning true when that counter equals zero,
or false if we hit the end of the string (when the string argument is empty and
the associated `AsList` is `Nil`) while the counter is still non-zero.

If the counter is non-zero and the string is non-empty, we check the current `c`
character to see if it is a vowel, by checking to see if our `vowels` list
contains it, then recurse, decrementing the counter if it was a vowel, and
leaving the counter unchanged if it wasn't.

The use of `| xs` after the recursive call to `containsVowels` tells Idris to
recurse directly to the `with` block, allowing it to reuse the `AsList` value in
`xs` without having to generate the `AsList` view again.

```idris
containsVowels : (count : Nat) -> String -> Bool
containsVowels count str with (asList str)
  containsVowels 0 str | _ = True
  containsVowels (S k) "" | [] = False
  containsVowels (S k) (strCons c str) | (c :: xs) = 
    if any (== c) vowels
      then containsVowels k str | xs
      else containsVowels (S k) str | xs
```

### At least one letter appears twice in a row

For this one, since we need to inspect two letters at a time, we break out a
nested `with` block, with the tail of the `AsList` as the argument of the block,
to also pattern match on the next character of the string.

Since the `AsList` view is lazy, we need to use `force` in the inner with block
to force the evaluation of the next component of the view, this is due to a
[bug in the compiler](https://github.com/idris-lang/Idris2/issues/3461).

The logic here is pretty simple, if we hit the empty string or get down to one
character, return `False`, if we have two characters available, compare them,
returning `True` if they match, and recursing to the outer with block, only
consuming one of the two characters, if they don't match.

```idris
doubleLetter : String -> Bool
doubleLetter str with (asList str)
  doubleLetter "" | [] = False
  doubleLetter (strCons c str) | (c :: x) with (force x)
    doubleLetter (strCons c "") | (c :: x) | [] = False
    doubleLetter (strCons c (strCons d str)) | (c :: x) | (d :: y) = 
      if c == d
        then True
        else doubleLetter (strCons d str) | x
```

### No Invalid Substrings

First we define the substrings that are disallowed

```idris
disallowedSubstrs : List String
disallowedSubstrs = ["ab", "cd", "pq", "xy"]
```

Idris's standard library does not currently define a function to check if a
string is a substring of another, so we instead use our own `isSubstr` function,
defined via use of the `AsList` view, from our [Util](../../Util.md#issubstr)
module.

```idris
noDisallowed : String -> Bool
noDisallowed str = 
  not $ any (`isSubstr` str) disallowedSubstrs
```

### isNice

Combine all three of our above functions together to check if a string is a
"nice" string

```idris
isNice : String -> Bool
isNice str = containsVowels 3 str && doubleLetter str && noDisallowed str
```

## New niceness

### Pair of letters that appears twice

Use a similar approach to `doubleLetter` above, but instead of comparing the two
chars for equality, pack them into a string and check if they are a substring of
the rest of the string.

```idris
pairTwice : String -> Bool
pairTwice str with (asList str)
  pairTwice "" | [] = False
  pairTwice (strCons c str) | (c :: x) with (force x)
    pairTwice (strCons c "") | (c :: x) | [] = False
    pairTwice (strCons c (strCons d str)) | (c :: x) | (d :: y) = 
      if pack [c, d] `isSubstr` str
        then True
        else pairTwice (strCons d str) | x
```

### Letter that repeats after one letter

More of the same, but this one gets extra fun because we are matching 3 letters
at a time. This would be a lot nicer if we could get away without nesting the
`with` blocks, but due to the aformentioned compiler bug, we need the nesting.

```idris
letterRepeatGap : String -> Bool
letterRepeatGap str with (asList str)
  letterRepeatGap "" | [] = False
  letterRepeatGap (strCons c str) | (c :: x) with (force x)
    letterRepeatGap (strCons c "") | (c :: x) | [] = False
    letterRepeatGap (strCons c (strCons d str)) | (c :: x) | (d :: y) with (force y)
      letterRepeatGap (strCons c (strCons d "")) | (c :: x) | (d :: y) | [] = False
      letterRepeatGap (strCons c (strCons d (strCons e str))) | (c :: x) | (d :: y) | (e :: z) = 
        if c == e
          then True
          else letterRepeatGap (strCons d (strCons e str)) | x
```

### New isNice

Glue our two new niceness functions together

```idris
isNice' : String -> Bool
isNice' str = pairTwice str && letterRepeatGap str
```

## Part Functions

### Part 1

Split our input up into a list of its component strings, and then count how many
satisfy the "nice" criteria.

```idris
part1 : Eff (PartEff String) (Nat, ())
part1 = do
  strings <- map (lines . trim) $ askAt "input"
  let x = count isNice strings
  pure (x, ())
```

### Part 2

Same as above, but with the new niceness criteria

```idris
part2 : () -> Eff (PartEff String) Nat
part2 _ = do
  strings <- map (lines . trim) $ askAt "input"
  let x = count isNice' strings
  pure x
```

```idris hide
public export
day5 : Day
day5 = Both 5 part1 part2
```