From f2070b7513b11e4324a4c73e42298955be65dc2b Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 7 Jan 2025 13:03:31 -0500
Subject: [PATCH] Year 2015 Day 5 Part 2

---
 src/Years/Y2015/Day5.md | 61 +++++++++++++++++++++++++++++++++++++++--
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md
index d7f1ad7..ba47358 100644
--- a/src/Years/Y2015/Day5.md
+++ b/src/Years/Y2015/Day5.md
@@ -85,7 +85,7 @@ 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'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
@@ -102,6 +102,51 @@ 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.
+
+```idris
+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.
+
+```idris
+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
+
+```idris
+isNice' : String -> Bool
+isNice' str = pairTwice str && letterRepeatGap str
+```
+
 ## Part Functions
 
 ### Part 1
@@ -116,8 +161,20 @@ part1 = do
   pure (x, ())
 ```
 
+### Part 2
+
+Same as above, but with the new niceness criteria
+
+```idris
+part2 : () -> Eff (PartEff String) Nat
+part2 _ = do
+  strings <- map (lines . trim) $ askAt "input"
+  let x = count isNice' strings
+  pure x
+```
+
 <!-- idris
 public export
 day5 : Day
-day5 = First 5 part1
+day5 = Both 5 part1 part2
 -->