Year 2015 Day 5 Part 1

README.md

@@ -22,3 +22,4 @@ The goal of this project is to get all 500 currently available stars in the form
   - [Day 2](src/Years/Y2015/Day2.md)
   - [Day 3](src/Years/Y2015/Day3.md)
   - [Day 4](src/Years/Y2015/Day4.md)
+  - [Day 5](src/Years/Y2015/Day5.md)

src/Years/Y2015.md

@@ -10,6 +10,7 @@ import Years.Y2015.Day1
 import Years.Y2015.Day2
 import Years.Y2015.Day3
 import Years.Y2015.Day4
+import Years.Y2015.Day5
 -->
 
 # Days
@@ -38,12 +39,18 @@ y2015 = MkYear 2015 [
   , day3
 ```
 
-## [Day 4](Y2015/Day3.md)
+## [Day 4](Y2015/Day4.md)
 
 ```idris
   , day4
 ```
 
+## [Day 5](Y2015/Day5.md)
+
+```idris
+  , day5
+```
+
 ```idris
   ]
 ```

src/Years/Y2015/Day5.md

@@ -0,0 +1,123 @@
+# 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
+module Years.Y2015.Day5
+
+import Control.Eff
+
+import Runner
+-->
+
+```idris
+import Data.String
+
+import Util
+```
+
+<!-- idris
+%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
+```
+
+## 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, ())
+```
+
+<!-- idris
+public export
+day5 : Day
+day5 = First 5 part1
+-->