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