Year 2015 Day 5
This day provides a nice chance to introduce
views,
specifically String's
AsList
view, which lets us treat Strings as if they were lazy lists or iterators.
import Data.String
import Util
Nice Strings
Contains at least 3 vowels
First we must define what a vowel is
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 strConsing 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.
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.
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.
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
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
module.
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
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.
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.
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
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.
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
part2 : () -> Eff (PartEff String) Nat
part2 _ = do
strings <- map (lines . trim) $ askAt "input"
let x = count isNice' strings
pure x