------------------------------------------------------------------------
-- The Agda standard library
--
-- Printf
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Text.Printf where
 
open import Data.String.Base using (String; fromChar; concat)
open import Function.Base using (id)
 
import Data.Integer.Show as ℤ
import Data.Float.Base   as Float
import Data.Nat.Show     as ℕ
 
open import Text.Format as Format hiding (Error)
open import Text.Printf.Generic
 
printfSpec : PrintfSpec formatSpec String
printfSpec .PrintfSpec.renderArg ℕArg      = ℕ.show
printfSpec .PrintfSpec.renderArg ℤArg      = ℤ.show
printfSpec .PrintfSpec.renderArg FloatArg  = Float.show
printfSpec .PrintfSpec.renderArg CharArg   = fromChar
printfSpec .PrintfSpec.renderArg StringArg = id
printfSpec .PrintfSpec.renderStr           = id
 
module Printf = Type formatSpec
open Printf public hiding (map)
open Render printfSpec public renaming (printf to gprintf)
 
printf : (fmt : String) → Printf (lexer fmt) String
printf fmt = Printf.map (lexer fmt) concat (gprintf fmt)