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