diff --git a/src/Util.md b/src/Util.md index c7a9bbc..836a4cd 100644 --- a/src/Util.md +++ b/src/Util.md @@ -9,24 +9,10 @@ module Util import Data.SortedSet import Data.String import Data.List.Lazy -import Data.List1 %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 This module provides views and associated functionality for treating `Integers` @@ -27,20 +26,19 @@ to prove properties about primitive types. mutual --> -## Primitive functionality +## Primative functionality Take the integer log base 10 of an `Integer` ```idris log10 : Integer -> Nat - log10 i = assert_total $ log10' i 0 + log10 i = 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 + if 10 ^ acc > i + then acc + else log10' i (acc + 1) ``` ## Ascending Order @@ -91,12 +89,12 @@ Generate an `Ascending` from an integer. export ascending : (i : Integer) -> Ascending i ascending i = - if i < 0 then NegAsc (ascending (assert_smaller i $ negate i)) else + if i < 0 then NegAsc (ascending (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)) + else believe_me $ Next digit rest (ascending rest) ``` Convert an `Ascending` to a list @@ -162,7 +160,7 @@ Generate a `Descending` from an `Integer` export descending : (i : Integer) -> Descending i descending i = - if i < 0 then NegDec (descending (assert_smaller i $ negate i)) else + if i < 0 then NegDec (descending (negate i)) else let magnitude = log10 i in if magnitude == 0 then believe_me $ Prev 0 0 0 Start diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 8a7b278..0225c82 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -16,7 +16,6 @@ import Years.Y2015.Day6 import Years.Y2015.Day7 import Years.Y2015.Day8 import Years.Y2015.Day9 -import Years.Y2015.Day10 --> # Days @@ -81,12 +80,6 @@ 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 deleted file mode 100644 index da03797..0000000 --- a/src/Years/Y2015/Day10.md +++ /dev/null @@ -1,114 +0,0 @@ -# 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, ()) -``` - -