Type-safe printf in Agda

type-safe-printf.agda

{-# OPTIONS --termination-depth=2 #-}

module Printf where

open import Algebra.FunctionProperties using (Associative)
open import Data.Char using (Char) renaming (_≟_ to _≟ᶜ_)
open import Data.List using (List; []; _∷_; [_]; length)
open import Data.Maybe
open import Data.Nat using (ℕ; suc)
open import Data.Nat.Show using (show)
open import Data.Product using (Σ; ∃; _,_; ,_; proj₁; proj₂)
open import Data.String using (String) renaming (_++_ to _++ˢ_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary using (yes; no)

module S = Data.String

-- Because Strings are primitive values we need to lean on the `trustMe'
-- escape hatch.  All the asserted properties are quite simple; please verify
-- them.
module TrustedKernel where
  open import Relation.Binary.PropositionalEquality.TrustMe

  -- Any string which is the empty list under toList, must be the empty
  -- string.
  toList-nil : {s : String} → S.toList s ≡ [] → s ≡ ""
  toList-nil p = trustMe

  -- Any string which is a cons pair under toList, must be the string of
  -- length 1 containing the head char prepended to the rest of the chars as a
  -- string.
  toList-cons : {c : Char} {cs : List Char} (s : String)
              → S.toList s ≡ c ∷ cs
              → s ≡ S.fromList [ c ] ++ˢ S.fromList cs
  toList-cons s p = trustMe

  -- Converting from chars to a string and back doesn't change the chars.
  to∘from : (cs : List Char) → S.toList (S.fromList cs) ≡ cs
  to∘from cs = trustMe

  -- (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
  ++-assoc : Associative _≡_ _++ˢ_
  ++-assoc x y z = trustMe
open TrustedKernel


-- Value-level representation of types allowed in format strings.
data Type : Set where nat string : Type

-- Convert value level to type level
⟦_⟧ : Type → Set
⟦    nat ⟧ = ℕ
⟦ string ⟧ = String

-- Convert a list of types to a function type
--
--   ⟦ nat ∷ string ∷ nat ∷ [] ⟧⁺ ≡ ℕ → (String → (ℕ → String))
--
⟦_⟧⁺ : List Type → Set
⟦     [] ⟧⁺ = String
⟦ x ∷ xs ⟧⁺ = ⟦ x ⟧ → ⟦ xs ⟧⁺

-- Convert the value-level representation to what matches it in a format
-- string.
⟦_⟧ˢ : Type → String
⟦    nat ⟧ˢ = "n"
⟦ string ⟧ˢ = "s"

isType : (c : Char) → Maybe (Σ Type λ τ → S.fromList [ c ] ≡ ⟦ τ ⟧ˢ)
isType c with c ≟ᶜ 'n' | c ≟ᶜ 's'
isType .'n' | yes refl | yes ()
isType .'n' | yes refl | no    ¬p = just (nat    , refl)
isType .'s' | no    ¬p | yes refl = just (string , refl)
isType c    | no    ¬p | no   ¬p₁ = nothing


-- Strings are a primitive type which can't be pattern matched.  This type
-- breaks a primitive String up into a List of Chars while maintaining a link
-- back to the original String in its type index.
data CharList : ℕ → String → Set where
  []  : CharList 0 ""
  _∷_ : ∀ c {n s} → CharList n s → CharList (suc n) (S.fromList [ c ] ++ˢ s)

-- Conversion to CharList.
toList⁺ : ∀ s → CharList (length (S.toList s)) s
toList⁺ s with S.toList s | inspect S.toList s
toList⁺ s |     [] | Reveal_is_.[ eq ] =
  subst (CharList _) (sym (toList-nil eq)) []
toList⁺ s | c ∷ cs | Reveal_is_.[ eq ] =
  subst (CharList _) (sym (toList-cons _ eq)) (c ∷ (go cs))
  where
    go : ∀ xs →  CharList (length xs) (S.fromList xs)
    go [] = []
    go (c ∷ cs) = subst (CharList _) (sym prf) (c ∷ (go cs))
      where prf = toList-cons (S.fromList (c ∷ cs)) (to∘from (c ∷ cs))

-- An intermediate type, keeping track of where there are splits between
-- wildcard characters (%) and other chars.  The non-wildcards are kept as
-- strings.
data Printf : String → List Type → Set where
  []  : Printf "" []
  lit : ∀ {τs} s {ss} → Printf ss τs → Printf (s ++ˢ ss) τs
  var : ∀ τ {τs s} → Printf s τs → Printf ("%" ++ˢ ⟦ τ ⟧ˢ ++ˢ s) (τ ∷ τs)

-- Convert a String to a Printf value; the Type list is only known in the
-- return value.
prepare : ∀ (s : String) → Σ (List Type) (Printf s)
prepare s = go (toList⁺ s)
  where
  go-lit : ∀ {ss τs} s → Printf ss τs → Printf (s ++ˢ ss) τs
  go-lit s [] = lit s []
  go-lit s (lit ss x) = subst₂ Printf (++-assoc s _ _) refl (lit (s ++ˢ ss) x)
  go-lit s (var τ x) = lit s (var τ x)

  -- Recurse on the list of chars while maintaining the correct String index.
  -- Chars are also primitive so we can't pattern match on them either, have
  -- to use the clumsy _≟_ function instead.
  go : ∀ {n s} → CharList n s → ∃ (Printf s)
  go [] = [] , []
  go (c  ∷ cs) with c ≟ᶜ '%'
  go (._ ∷ []) | yes refl = _ , lit "%" []
  go (._ ∷ c ∷ cs) | yes refl with isType c
  go (._ ∷ c ∷ cs) | yes refl | just (τ , prf) =
    , subst₂ Printf p refl (var τ (proj₂ (go cs)))
    where p = cong (S._++_ "%") (cong₂ S._++_ (sym prf) refl)
  go (._ ∷ c ∷ cs) | yes refl | nothing = , go-lit "%" (proj₂ (go (c ∷ cs)))
  go (c ∷ cs) | no ¬p = , go-lit (S.fromList [ c ]) (proj₂ (go cs))

-- Two tricky little functions that prepend a value to the result of a
-- function which can have any number of arguments.
private
  prepend : ∀ {τs} → String → ⟦ τs ⟧⁺ → ⟦ τs ⟧⁺
  prepend {   []} s xs = s ++ˢ xs
  prepend {_ ∷ _} s  f = λ x → prepend s (f x)

  prepend-fn : ∀ {τ τs} → (⟦ τ ⟧ → String) → ⟦ τs ⟧⁺ → ⟦ τ ∷ τs ⟧⁺
  prepend-fn {_} {   []} f s = λ x → f x ++ˢ s
  prepend-fn {_} {_ ∷ _} f g = λ x → prepend (f x) g

-- Turn a Printf value into an actual function that can be called with ℕ and
-- String values to fill the wildcards.
execute : ∀ {s} → (x : ∃ (Printf s)) → ⟦ proj₁ x ⟧⁺
execute ([] , []) = ""
execute (_       , lit s      xs) = prepend s            (execute (_ , xs))
execute (._ ∷ τs , var    nat xs) = prepend-fn show      (execute (_ , xs))
execute (._ ∷ τs , var string xs) = prepend-fn (λ x → x) (execute (_ , xs))

printf : (s : String) → ⟦ proj₁ (prepare s) ⟧⁺
printf = execute ∘ prepare


-- A quick example.
example : ℕ → String → String
example = printf "foo %n bar %s quux"

example-proof : example 10 "abc" ≡ "foo 10 bar abc quux"
example-proof = refl