From fe4a20ade6527c8c61139489b199fae0c745fcf7 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 19 Jan 2025 22:05:30 -0500 Subject: [PATCH 1/4] Add Util.Digits modules Contains views for seeing integers as lists of digits --- advent.ipkg | 1 + src/Util/Digits.md | 192 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 193 insertions(+) create mode 100644 src/Util/Digits.md diff --git a/advent.ipkg b/advent.ipkg index 1ac1a6e..e915d93 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -26,6 +26,7 @@ depends = base modules = Runner , Util , Util.Eff + , Util.Digits , Grid -- main file (i.e. file to load at REPL) diff --git a/src/Util/Digits.md b/src/Util/Digits.md new file mode 100644 index 0000000..4cf58b0 --- /dev/null +++ b/src/Util/Digits.md @@ -0,0 +1,192 @@ +# Viewing Integers as lists of digits + +```idris +module Util.Digits + +import Data.Monoid.Exponentiation +``` + + + +This module provides views and associated functionality for treating `Integers` +as if they were lists of numbers. + +Since `Integer` is a primitive type, that Idris can't directly reason about the +structure of, we need to use some `believe_me`s, a hideously unsafe operation +that completely bypasses the type checker, somewhere along the line. For +teaching purposes, we'll do it here, but please consider a library like +[prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing +to prove properties about primitive types. + + + +## Primitive functionality + +Take the integer log base 10 of an `Integer` + +```idris + log10 : Integer -> Nat + log10 i = assert_total $ log10' i 0 + where + covering + log10' : Integer -> (acc : Nat) -> Nat + log10' i acc = + if i > 0 + then log10' (i `div` 10) (S acc) + else acc +``` + +## Ascending Order + +View an integer as a list of digits, ordered from least significant digit to +most significant digit. + +For a clarifying example: + + + +```idris + ascList (ascending 12345) == [5, 4, 3, 2, 1] +``` + +The view itself, storing the current digit, and the rest of the number, both as +a raw integer and by a recursive `Ascending`. Acts as a proof that the number +can be reproduced by multiplying the rest by 10 and then adding the current +digit. + +```idris + ||| A view of an integer as a list of digits in order of ascending signifigance + public export + data Ascending : Integer -> Type where + ||| Indicates that the number was negative + NegAsc : (rec : Lazy (Ascending (negate i))) -> Ascending i + ||| Indicates we have already seen all the digits of a number + End : Ascending 0 + ||| A digit and all the preceeding ones + Next : (digit : Integer) + -> (rest : Integer) + -> (rec : Lazy (Ascending rest)) + -> Ascending (rest * 10 + digit) + %name Ascending as, bs, cs +``` + +Generate an `Ascending` from an integer. + +```idris + ||| Covering function for `Ascending` + export + ascending : (i : Integer) -> Ascending i + ascending i = + if i < 0 then NegAsc (ascending (assert_smaller i $ negate i)) else + let digit = i `mod` 10 + rest = i `div` 10 + in if rest == 0 + then believe_me $ Next digit rest (believe_me End) + else believe_me $ Next digit rest (ascending (assert_smaller i rest)) +``` + +Convert an `Ascending` to a list + +```idris + export + ascList : {i : Integer} -> Ascending i -> List Integer + ascList as = reverse $ ascList' i as [] + where + ascList' : (j : Integer) -> Ascending j -> (acc : List Integer) + -> List Integer + ascList' k (NegAsc rec) acc = ascList' (negate k) rec acc + ascList' 0 End acc = acc + ascList' ((rest * 10) + digit) (Next digit rest rec) acc = + ascList' rest rec (digit :: acc) +``` + +## Descending Order + +View an integer as a list of digits, ordered from most significant digit to +least significant digit. + +For a clarifying example: + + + +```idris + decList (descending 12345) == [1, 2, 3, 4, 5] +``` + +The view itself, storing the current digit, and the rest of the number, both as +a raw integer and by a recursive `Ascending`. Acts as a proof that the number +can be reproduced by appending the current digit to the rest of the number. + +```idris + ||| A view of an integer as a list of digits in order of descending + ||| signifigance + public export + data Descending : Integer -> Type where + ||| Indicates that the number was negative + NegDec : (rec : Lazy (Descending (negate i))) -> Descending i + ||| Indicates we have already seen all the digits of a number + Start : Descending 0 + ||| A digit and all the preceeding ones + Prev : (magnitude : Nat) + -> (digit : Integer) + -> (rest : Integer) + -> (rec : Lazy (Descending rest)) + -> Descending ((digit * 10 ^ magnitude) + rest) + %name Descending ds, es, fs +``` + +Generate a `Descending` from an `Integer` + +```idris + export + descending : (i : Integer) -> Descending i + descending i = + if i < 0 then NegDec (descending (assert_smaller i $ negate i)) else + let magnitude = log10 i + in if magnitude == 0 + then believe_me $ Prev 0 0 0 Start + else descending' magnitude i + where + descending' : (magnitude : Nat) -> (j : Integer) -> Descending j + descending' 0 j = believe_me Start + descending' magnitude@(S m) j = + let digit = j `div` 10 ^ m + rest = j - digit * 10 ^ m + in believe_me $ Prev m digit rest (descending' m rest) +``` + +Convert a `Descending` to a list + +```idris + export + decList : {i : Integer} -> Descending i -> List Integer + decList ds = reverse $ decList' ds [] + where + decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> + List Integer + decList' (NegDec rec) acc = decList' rec acc + decList' Start acc = acc + decList' (Prev magnitude digit rest rec) acc = + decList' rec (digit :: acc) +``` From 12305cc232f669be4a519530893d1ba9b570b681 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 20 Jan 2025 00:07:50 -0500 Subject: [PATCH 2/4] Add repeatN to Util --- src/Util.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Util.md b/src/Util.md index 836a4cd..62d4a83 100644 --- a/src/Util.md +++ b/src/Util.md @@ -13,6 +13,19 @@ import Data.List.Lazy %default total ``` +## Functions + +### repeatN + +Recursively applies `f` to `seed` N times + +```idris +export +repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a +repeatN 0 f seed = seed +repeatN (S times') f seed = repeatN times' f (f seed) +``` + ## Either # Days @@ -80,6 +81,12 @@ y2015 = MkYear 2015 [ , day9 ``` +## [Day 10](Y2015/Day10.md) + +```idris + , day10 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day10.md b/src/Years/Y2015/Day10.md new file mode 100644 index 0000000..da03797 --- /dev/null +++ b/src/Years/Y2015/Day10.md @@ -0,0 +1,114 @@ +# Year 2015 Day 10 + +This day doesn't really add anything new, but we will show off our new views for +viewing integers as lists of digits. + + + +```idris +import Data.String +import Data.List1 +import Data.List.Lazy +import Data.Monoid.Exponentiation +import Data.Nat.Views + +import Util +import Util.Digits +``` + + + +# Solver Functions + +Produce a lazy lists of the digits of a number, in descending order of +significance. This effectively translates our new +[`Descending`](../../Util/Digits.md) view to a `LazyList`. + +```idris +lazyDigits : Integer -> LazyList Integer +lazyDigits i with (descending i) + lazyDigits i | (NegDec rec) = lazyDigits _ | rec + lazyDigits 0 | Start = [] + lazyDigits ((digit * (10 ^ magnitude)) + rest) | (Prev _ digit rest rec) = + digit :: lazyDigits _ | rec +``` + +Apply the look-and-say rule to list of digits. We operate in the list-of-digits +space for efficiency, this number will grow into the hundreds of thousands of +digits, and Idris is currently lacking some needed primitive operations to +perform this operation in `Integer` space reasonably efficiently. A `LazyList` +is used here to avoid having to actually instantiate the entirety of these +reasonably large lists. + +```idris +lookAndSay : LazyList Integer -> LazyList Integer +lookAndSay digits = + -- Flatten the list once more + lazyConcat + -- Convert the produced numbers into lists of their digits + . map lazyDigits + -- re-flatten our list + . lazyConcat + -- Count the number of occurrences of each digit and emit [occurances, digit] + . map (\xs@(head ::: tail) => + (the (LazyList _) [natToInteger $ length xs, head])) + -- Group identical digits + . lazyGroup + $ digits +``` + +Apply the look-and-say rule to an integer, for repl testing + +```idris +lookAndSay' : Integer -> Integer +lookAndSay' i = + let digits = lazyDigits i + res = lookAndSay digits + in unDigits res 0 + where + unDigits : LazyList Integer -> (acc : Integer) -> Integer + unDigits [] acc = acc + unDigits (x :: xs) acc = unDigits xs (acc * 10 + x) +``` + +Repeatedly apply `lookAndSay` to a seed value, with logging + +```idris +repeatLogged : Has Logger fs => + (count : Nat) -> (seed : LazyList Integer) -> Eff fs $ LazyList Integer +repeatLogged 0 seed = pure seed +repeatLogged (S k) seed = do + trace "Remaining iterations: \{show (S k)} digits: \{show . count (const True) $ seed}" + repeatLogged k (lookAndSay seed) +``` + +# Part Functions + +## Part 1 + +Parse our input, convert it into a list of digits, then run our `lookAndSay` +function on it 40 times, and count the output digits. + +```idris +part1 : Eff (PartEff String) (Nat, ()) +part1 = do + input <- askAt "input" >>= (note "Invalid input" . parsePositive) + let input = lazyDigits input + info "Input: \{show input}" + output <- repeatLogged 40 input + pure (count (const True) output, ()) +``` + +