From 6c757cfde712e9f0dda1b93d1dae5df76676950c Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Tue, 7 Jan 2025 11:47:05 -0500 Subject: [PATCH] Year 2015 Day 5 Part 1 --- README.md | 1 + src/Years/Y2015.md | 9 ++- src/Years/Y2015/Day5.md | 123 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 132 insertions(+), 1 deletion(-) create mode 100644 src/Years/Y2015/Day5.md diff --git a/README.md b/README.md index 5d485c3..07336c6 100644 --- a/README.md +++ b/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) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 848935a..5fb0cd3 100644 --- a/src/Years/Y2015.md +++ b/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 ] ``` diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md new file mode 100644 index 0000000..d7f1ad7 --- /dev/null +++ b/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 +import Data.String + +import Util +``` + + + +## 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, ()) +``` + +