    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Generic printf function.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Text.Printf.Generic where

    open import Level using (Level; 0ℓ; _⊔_; Lift)
    open import Data.List.Base as List using (List; []; _∷_)
    open import Data.Char.Base
    open import Data.Maybe.Base hiding (map)
    open import Data.Nat.Base using (ℕ)
    open import Data.Product.Base hiding (map)
    open import Data.Product.Nary.NonDependent
    open import Data.String.Base using (String)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
    open import Data.Unit.Base using (⊤)
    open import Function.Nary.NonDependent
    open import Function.Base

    open import Text.Format.Generic

    private
      variable
        ℓ : Level
        A B : Set ℓ

    ------------------------------------------------------------------------
    -- Printf argument specifications.
    -- Defines the rendering of chunks.

    record PrintfSpec {ℓ} (spec : FormatSpec) (A : Set ℓ) : Set (Level.suc 0ℓ ⊔ ℓ) where

      open FormatSpec spec public

      field
        renderArg : ∀ arg → ArgType arg → A
        renderStr : String → A

    module Type (spec : FormatSpec) where

      open Format spec renaming (Error to FormatError)

      record Error (e : FormatError) : Set ℓ where

      private

        Size : FormatError ⊎ Format → ℕ
        Size (inj₁ err) = 0
        Size (inj₂ fmt) = size fmt

      Printf : ∀ pr → Set ℓ → Set (ℓ ⊔ ⨆ (Size pr) 0ℓs)
      Printf (inj₁ err) _ = Error err
      Printf (inj₂ fmt) B = Arrows _ ⟦ fmt ⟧ B

      map : ∀ pr → (A → B) → Printf pr A → Printf pr B
      map (inj₁ err) f p = _
      map (inj₂ fmt) f p = mapₙ _ f p

    module Render {spec : FormatSpec} (render : PrintfSpec spec A) where

      open PrintfSpec render
      open Type spec

      open Format spec renaming (Error to FormatError)

      assemble : ∀ fmt → Product⊤ _ ⟦ fmt ⟧ → List A
      assemble [] vs                    = []
      assemble (Arg a   ∷ fmt) (x , vs) = renderArg a x ∷ assemble fmt vs
      assemble (Raw str ∷ fmt) vs       = renderStr str ∷ assemble fmt vs

      private

        printf′ : ∀ pr → Printf pr (List A)
        printf′ (inj₁ err) = _
        printf′ (inj₂ fmt) = curry⊤ₙ _ (assemble fmt)

      printf : (input : String) → Printf (lexer input) (List A)
      printf input = printf′ (lexer input)