sprintf.lagda

*Note*: I will call this ~sprintf~ instead of ~printf~ since we are not dealing with IO.
I will use the terminology from the [[https://linux.die.net/man/3/fprintf][man page for ~sprintf~]].
~sprintf~ takes a "format string" which is any number of "directives".
A directive is either a character other than ~'%'~ or a "conversion specification" consisting of a ~'%'~ and conversion specifier (such as ~d~ for integers).

The design chosen during lecture failed since our level of abstraction was at characters instead of directives.
For instance, the string ~"%d"~ has two characters but only a single directive: the integer conversion specification.

We can start with a data type to represent directives.

\begin{code}
data Directive : Set where
  CInteger    : Directive
  CChar       : Directive
  CImpossible : Directive
  Ordinary    : Char → Directive
\end{code}

Next we need to transform a list of characters into a list of ~Directive~s.
Some noteworthy edge cases:

* To get a literal ~'%'~ you must use ~"%%"~ in your format string.
* Unsupported conversion specifications will yield a function which accepts an empty type.
* Ending a format string with the start of a conversion specification will simply ignore it.

\begin{code}
formatString : List Char → List Directive
formatString = f Default
  where
    -- This is a little extra, but it stops us from repeating the '%' pattern match
    -- over and over again.
    data State : Set where
      Default : State
      InSpecification : State

    conversionSpecifier : Char → Directive
    conversionSpecifier 'd' = CInteger
    conversionSpecifier 'c' = CChar
    conversionSpecifier '%' = Ordinary '%'
    conversionSpecifier _   = CImpossible

    f : State → List Char → List Directive
    f s [] = []
    f Default ('%' ∷ cs)       = f InSpecification cs
    f Default (c ∷ cs)         = Ordinary c ∷ f Default cs
    f InSpecification (c ∷ cs) = conversionSpecifier c ∷ f Default cs

_ : formatString (primStringToList "%d") ≡ CInteger ∷ []
_ = definition-chasing

_ : formatString (primStringToList "P %%%d %c%") ≡
      Ordinary 'P' ∷ Ordinary ' ' ∷ Ordinary '%' ∷ CInteger ∷ Ordinary ' ' ∷ CChar ∷ []
_ = definition-chasing
\end{code}

We need to convert a directive into a type which Agda understands.

\begin{code}
reify : Directive → Set
reify CInteger = ℕ
reify CChar    = Char
reify _        = ⊥
\end{code}

Now we must produce a function type given a ~List Directive~.

\begin{code}
directivesToType : List Directive → Set
directivesToType [] = String
directivesToType (Ordinary _ ∷ ds) = directivesToType ds
directivesToType (d ∷ ds) = reify d → directivesToType ds

_ : directivesToType (formatString (primStringToList "%d %c")) ≡ (ℕ → Char → String)
_ = definition-chasing

_ : directivesToType (formatString (primStringToList "%c %a")) ≡ (Char → ⊥ → String)
_ = definition-chasing
\end{code}

This lets us specify the type of ~sprintf~.

\begin{code}
sprintf : (fmt : String) → directivesToType (formatString (primStringToList fmt))
sprintf = sprintf₁ "" ∘ formatString ∘ primStringToList
  where
    sprintf₁ : String → (dirs : List Directive) → directivesToType dirs
    sprintf₁ s [] = s
    sprintf₁ s (CInteger ∷ dirs) x    = sprintf₁ (s ++ NatShow.show x) dirs
    sprintf₁ s (CChar ∷ dirs) x       = sprintf₁ (s ++ primStringFromList (x ∷ [])) dirs
    sprintf₁ s (CImpossible ∷ dirs) ⊥ = sprintf₁ s dirs
    sprintf₁ s (Ordinary x ∷ dirs)    = sprintf₁ (s ++ primStringFromList (x ∷ [])) dirs

_ : sprintf (primStringFromList ('%' ∷ 'd' ∷ ' ' ∷ '%' ∷ 'c' ∷ [])) 5 'a' ≡ primStringFromList ('5' ∷ ' ' ∷ 'a' ∷ [])
_ = definition-chasing

{- You cannot fill me!
_ : sprintf (primStringFromList ('%' ∷ 'a' ∷ [])) {!!} ≡ {!!}
_ = definition-chasing
-}
\end{code}