I am not bored at work, I am exploring dependently-typed programming in practical settings.......

AocDay1.idr

module AocDay1

import Decidable.Equality
import Data.List.Quantifiers
import Data.Singleton
import Data.String

data Length : Any p xs -> Nat -> Type  where
  Here : Length (Here p)  Z
  There : Length ltr n
       -> Length (There ltr) (S n)

length : (prf : Any p xs) -> DPair Nat (Length prf)
length (Here x)
  = (0 ** Here)
length (There x) with (length x)
  length (There x) | (fst ** snd)
    = (S fst ** There snd)


positiveAny : (xs : List Char)
       -> (c  : Char)
             -> Either (All (Not . Equal c) xs)
                       (Any (      Equal c) xs)
positiveAny [] c
  = Left []
positiveAny (x :: xs) c with (decEq c x)
  positiveAny (c :: xs) c | (Yes Refl)
    = Right (Here Refl)
  positiveAny (x :: xs) c | (No contra) with (positiveAny xs c)
    positiveAny (x :: xs) c | (No contra) | (Left prf)
      = Left (contra :: prf)
    positiveAny (x :: xs) c | (No contra) | (Right prf)
      = Right (There prf)

data SafeHT : List a -> Maybe (a,a) -> Type where
  NEmpty : SafeHT Nil Nothing

  NOne   : SafeHT [x] (Just (x,x))

  NCons  : SafeHT      xs  (Just (a,l))
        -> SafeHT (x::xs) (Just (x,l))

safeHT : (xs : List a) -> DPair (Maybe (a,a)) (SafeHT xs)
safeHT []
  = (Nothing ** NEmpty)

safeHT (x :: [])
  = (Just (x, x) ** NOne)

safeHT (x :: (y :: xs)) with (safeHT (y::xs))
  safeHT (x :: (y :: [])) | ((Just (y, y)) ** NOne)
    = (Just (x, y) ** NCons NOne)
  safeHT (x :: (y :: xs)) | ((Just (y, l)) ** (NCons z))
    = (Just (x, l) ** NCons (NCons z))

CharPred : Type
CharPred = Char -> Type

ValidDigits : List Char
ValidDigits
  = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']

IsDigit : CharPred
IsDigit c
  = Any (Equal c) ValidDigits

IsDigitNot : CharPred
IsDigitNot c
  = All (Not . Equal c) ValidDigits

isDigit : (c : Char) -> Either (IsDigitNot c) (IsDigit c)
isDigit = positiveAny ValidDigits

data Line : (inputs : List Char)
         -> (digits : List Nat)
         -> (cigits : List Char)
         -> Type
  where
    Empty : Line Nil Nil Nil
    Skip : (IsDigitNot c)
        -> Line     is  ds     cs
        -> Line (c::is) ds (c::cs)
    Digi : (prf : IsDigit c)
        -> Length prf l
        -> Line is ds cs
        -> Line (c::is) (l::ds) cs


line : (inputs : List Char)
    -> (cs ** ds ** Line inputs ds cs)
line [] = ([] ** ([] ** Empty))
line (x :: xs) with (Day1.isDigit x)
  line (x :: xs) | result_c with (line xs)
    line (x :: xs) | (Left prf) | (cs ** ds ** spec)
      = (x :: cs ** (ds ** Skip prf spec))

    line (x :: xs) | (Right prf) | (cs ** ds ** spec) with (length prf)
      line (x :: xs) | (Right prf) | (cs ** ds ** spec) | (l ** prfL)
        = (cs ** (l :: ds ** Digi prf prfL spec))

data Lines : (inputs : List (List Char))
          -> (digits : List (List Nat))
                    -> Type
  where
    LEmpty : Lines Nil Nil
    CLine : Line  i  d  cs
         -> Lines is ds
         -> Lines (i::is) (d::ds)

lines : (inputs : List (List Char))
     -> DPair (List (List Nat))
              (Lines inputs)
lines []
  = ([] ** LEmpty)
lines (x :: xs) with (line x)
  lines (x :: xs) | (cs ** ds ** prfL) with (lines xs)
    lines (x :: xs) | (cs ** ds ** prfL) | (rest ** prfR)
      = (ds :: rest ** CLine prfL prfR)

data SumHT : List (List Nat) -> Nat -> Type where
  SEmpty : SumHT Nil 0
  SCons : SafeHT n (Just (h,t))
       -> SumHT  ns res
       -> SumHT  (n::ns) ((h * 10) `plus` (plus t res))
  SSkip : SafeHT n Nothing
       -> SumHT ns res
       -> SumHT (n::ns) res

sumHT : (ds : List (List Nat)) -> DPair Nat (SumHT ds)
sumHT []
  = (0 ** SEmpty)
sumHT (x :: xs) with (safeHT x)
  sumHT (x :: xs) | (fst ** prfHT) with (fst)
    sumHT (x :: xs) | (fst ** prfHT) | a with (sumHT xs)
      sumHT (x :: xs) | (fst ** prfHT) | Nothing | (y ** snd) = (y ** SSkip prfHT snd)
      sumHT (x :: xs) | (fst ** prfHT) | (Just (z, w)) | (y ** snd)
        = (plus (z * 10) (plus w y) ** SCons prfHT snd)

data Extract : String -> Nat -> Type where
  E : Lines (map (Types.unpack . String.trim) (lines input))
            values
   -> SumHT values result
   -> Extract input result

extract : (str : String) -> DPair Nat (Extract str)
extract str with (lines (map (unpack . trim) (lines str)))
  extract str | (ds ** prfL) with (sumHT ds)
    extract str | (ds ** prfL) | (res ** prfS)
      = (res ** E prfL prfS)

testDoc : String
testDoc =
  """
  1abc2
  pqr3stu8vwx
  a1b2c3d4e5f
  treb7uchet
  """

test : fst (extract Day1.testDoc) === 142
test = Refl