Year 2015 Day 11 Part 1

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)

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
   ]
 ```

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 
+module Years.Y2015.Day11
+
+import Control.Eff
+
+import Runner
+-->
+
+```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
+```
+
+<!-- idris
+Show PasswordChar where
+  show (MkPC char) = singleton char
+
+Eq PasswordChar where
+  x == y = x.char == y.char
+-->
+
+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, ())
+```
+
+<!-- idris
+public export
+day11 : Day
+day11 = First 11 part1
+-->
+
+[^1]: https://github.com/stefan-hoeck/idris2-refined/