advent/src/Util/Digits.md

Viewing Integers as lists of digits

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_mes, 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 if you find yourself needing to prove properties about primitive types.

Primitive functionality

Take the integer log base 10 of an Integer

  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:

    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.

  ||| 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.

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

  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:

    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.

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

  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

  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)