From 9489721e2905c920f61a7b466c1aade268779bec Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Wed, 22 Jan 2025 22:29:38 -0500 Subject: [PATCH] Year 2015 Day 11 Part 1 --- README.md | 1 + src/Years/Y2015.md | 7 ++ src/Years/Y2015/Day11.md | 225 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 233 insertions(+) create mode 100644 src/Years/Y2015/Day11.md diff --git a/README.md b/README.md index 95cd2ee..2ce05fb 100644 --- a/README.md +++ b/README.md @@ -39,3 +39,4 @@ solution. - [Day 8](src/Years/Y2015/Day8.md) - [Day 9](src/Years/Y2015/Day9.md) - [Day 10](src/Years/Y2015/Day10.md) + - [Day 11](src/Years/Y2015/Day11.md) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 8a7b278..f745517 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -17,6 +17,7 @@ import Years.Y2015.Day7 import Years.Y2015.Day8 import Years.Y2015.Day9 import Years.Y2015.Day10 +import Years.Y2015.Day11 --> # Days @@ -87,6 +88,12 @@ y2015 = MkYear 2015 [ , day10 ``` +## [Day 11](Y2015/Day11.md) + +```idris + , day11 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day11.md b/src/Years/Y2015/Day11.md new file mode 100644 index 0000000..73820f1 --- /dev/null +++ b/src/Years/Y2015/Day11.md @@ -0,0 +1,225 @@ +# Year 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 +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 +``` + + + +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 +part1Critera : Vect n PasswordChar -> Bool +part1Critera 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, ()) +part1 = do + input <- map trim $ askAt "input" + password <- parsePassword input + info "Starting password: \{show password} -> \{passwordToString password}" + let next_password = findNextPassword part1Critera password + pure (passwordToString next_password, ()) +``` + + + +[^1]: https://github.com/stefan-hoeck/idris2-refined/