Add Util.Digits modules

Contains views for seeing integers as lists of digits

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
 
 <!-- idris
@@ -181,32 +167,3 @@ cartProd x y =
     combine x [] rest = rest
     combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
-
-### Concat
-
-Lazily concatenate a LazyList of LazyLists
-
-```idris
-export
-lazyConcat : LazyList (LazyList a) -> LazyList a
-lazyConcat [] = []
-lazyConcat (x :: xs) = x ++ lazyConcat xs
-```
-
-### Group
-
-Lazily group a LazyList
-
-```idris
-export
-lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
-lazyGroup [] = []
-lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
-  where
-    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
-    lazyGroup' [] current acc = [acc]
-    lazyGroup' (y :: ys) current acc@(head ::: tail) = 
-      if y == current
-        then lazyGroup' ys current (head ::: (y :: tail))
-        else acc :: lazyGroup (y :: ys)
-```

src/Util/Digits.md

@@ -7,9 +7,8 @@ import Data.Monoid.Exponentiation
 ```
 
 <!-- idris
+-- TODO: Make these views sign-aware
 import System
-
-%default total
 -->
 
 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
+        if 10 ^ acc > i
-          then log10' (i `div` 10) (S acc)
+          then acc
-          else 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

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

src/Years/Y2015/Day10.md

@@ -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
-module Years.Y2015.Day10
-
-import Control.Eff
-
-import Runner
--->
-
-```idris
-import Data.String
-import Data.List1
-import Data.List.Lazy
-import Data.Monoid.Exponentiation
-import Data.Nat.Views
-
-import Util
-import Util.Digits
-```
-
-<!-- idris
-%default total
--->
-
-# 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, ())
-```
-
-<!-- idris
-public export
-day10 : Day
-day10 = First 10 part1
--->