------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of format strings and printf
------------------------------------------------------------------------

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

module README.Text.Printf where

open import Data.Nat.Base
open import Data.Char.Base
open import Data.List.Base
open import Data.String.Base
open import Data.Sum.Base

open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Format strings

open import Text.Format

-- We can specify a format by writing a string which will get interpreted
-- by a lexer into a list of formatting directives.

-- The specification types are always started with a '%' character:

-- Integers (%d or %i)
-- Naturals (%u)
-- Floats   (%f)
-- Chars    (%c)
-- Strings  (%s)

-- Anything which is not a type specification is a raw string to be spliced
-- in the output of printf.

-- For instance the following format alternates types and raw strings

_ : lexer "%s: %u + %u ≡ %u"
  ≡ inj₂ (`String ∷ Raw ": " ∷ `ℕ ∷ Raw " + " ∷ `ℕ ∷ Raw " ≡ " ∷ `ℕ ∷ [])
_ = refl

-- Lexing can fail. There are two possible errors:

-- If we start a specification type with a '%' but the string ends then
-- we get an UnexpectedEndOfString error

_ : lexer "%s: %u + %u ≡ %"
  ≡ inj₁ (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = refl

-- If we start a specification type with a '%' and the following character
-- does not correspond to an existing type, we get an InvalidType error
-- together with a focus highlighting the position of the problematic type.

_ : lexer "%s: %u + %a ≡ %u"
  ≡ inj₁ (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = refl

------------------------------------------------------------------------
-- Printf

open import Text.Printf

-- printf is a function which takes a format string as an argument and
-- returns a function expecting a value for each type specification present
-- in the format and returns a string splicing in these values into the
-- format string.

-- For instance `printf "%s: %u + %u ≡ %u"` is a
-- `String → ℕ → ℕ → ℕ → String` function.

_ : String → ℕ → ℕ → ℕ → String
_ = printf "%s: %u + %u ≡ %u"

_ : printf "%s: %u + %u ≡ %u" "example"   
  ≡ "example: 3 + 2 ≡ 5"
_ = refl

-- If the format string str is invalid then `printf str` will have type
-- `Error e` where `e` is the lexing error.

_ : Text.Printf.Error (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = printf "%s: %u + %u ≡ %"

_ : Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = printf "%s: %u + %a ≡ %u"

-- Trying to pass arguments to such an ̀Error` type will lead to a
-- unification error which hopefully makes the problem clear e.g.
-- `printf "%s: %u + %a ≡ %u" "example" 3 2 5` fails with the error:

-- Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u") should be
-- a function type, but it isn't
-- when checking that "example" 3 2 5 are valid arguments to a
-- function of type Text.Printf.Printf (lexer "%s: %u + %a ≡ %u")